p:FinProbSpace, n, m:. (n  m)  (C:p-open(p). E(n;s.C(<n, s>))  E(m;s.C(<m, s>))) 

latex

Definitions

, t  T, x:A. B(x), {x:A| B(x)} , x:AB(x), A  B, p-open(p), r  s, P  Q, False, A, , #$n, FinProbSpace, i  j , a < b, Void, -n, n+m, n - m, (i = j), Outcome, {i..j}, Type, x,y:A//B(x;y), RandomVariable(p;n), X  Y, SqStable(P), P & Q, type List, xL. P(x), x:A  B(x), A c B, True, T, Top, i  j < k, ||as||, , A  B, , if b then t else f fi , EquivRel(T;x,y.E(x;y)), tt, qeq(r;s), , x,y. t(x;y), s ~ t, {T}, SQType(T), null, <a, b>, f(a), x.A(x), E(n;F), , s = t, S  T, suptype(S; T), isint(z;a;b), case b of inl(x) => s(x) | inr(y) => t(y), P  Q, P  Q, i <z j, b, b, i z j, Unit, left + right, P  Q, Dec(P), x:A.B(x), a  b, , (x  l), x. t(x), l[i], a  j < b. E(j), rv-shift(x;X), t.2, cons-seq(x;s), t.1

Lemmas

nat sq, pi2 wf, pi1 wf, decidable le, cons-seq wf, ws-monotone, int seg properties, rv-shift wf, qsum wf, select wf, l all wf2, int inc rationals, l member wf, length wf1, top wf, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, not wf, decidable int equal, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, le int wf, assert wf, bnot wf, ifthenelse wf, lt int wf, natural number wf p-outcome, qle-int, decidable qle, qle wf, expectation wf, expectation-constant, quotient wf, bool wf, qeq wf2, btrue wf, b-union wf, int nzero wf, rationals wf, expectation-monotone, length wf nat, null-seq wf, sq stable from decidable, int-rational, int seg wf, p-outcome wf, ge wf, nat properties, finite-prob-space wf, p-open wf, le wf, nat wf